Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor of clauses #662

Merged
merged 5 commits into from
May 15, 2024
Merged

Refactor of clauses #662

merged 5 commits into from
May 15, 2024

Conversation

W95Psp
Copy link
Collaborator

@W95Psp W95Psp commented May 13, 2024

This PR implements the changes discussed in #661.

Fixes #661

@Nadrieril
Copy link
Collaborator

Nadrieril commented May 14, 2024

This is quite subtle because we need to make sure to either always hash the clause/predicate with its binder or never do that. Could you split this in a few commits that each do a single thing (e.g. 1. define PredicateId and its module, 2. cache the PredicateId inside Predicate, 3. change how we compute the ids wrt binders, etc).

@W95Psp
Copy link
Collaborator Author

W95Psp commented May 14, 2024

Yes, I'm gonna rebase this nicely, no worries!

After this PR, we should never compute a PredicateId from a type that has no binder (the ClauseId should enforce that)

@Nadrieril
Copy link
Collaborator

No problem, let me know when you have a version I can look at

@W95Psp W95Psp requested a review from Nadrieril May 15, 2024 06:48
W95Psp added 4 commits May 15, 2024 08:49
…`s and `Clause`s

In commit [fca56a], the type `Clause` has been renamed as
`ClauseKind`, then commit [21226e] makes `Clause` a
`Binder<ClauseKind>`, essentially (with an indirection via
`PredicateKind` and an invariant where the predicate kind has to be a
`ty::PredicateKind::Clause(ClauseKind)`).

That means that now, Rustc always provides `Clause` with
binders. Thus, it now makes sense to systematically compute clause
identifiers with binders.

Since clauses are a subset of predicates, we now always lift clauses
to predicates before computing identifiers. This was not possible
before, since we lacked binder information to properly lift clauses to
predicates

[fca56a]: rust-lang/rust@fca56a8
[21226e]: rust-lang/rust@21226ee
@W95Psp W95Psp marked this pull request as ready for review May 15, 2024 06:49
@W95Psp W95Psp added this pull request to the merge queue May 15, 2024
Merged via the queue into main with commit 4d4812a May 15, 2024
12 checks passed
@W95Psp W95Psp deleted the clauses-661 branch May 15, 2024 09:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
No open projects
Status: Done
Development

Successfully merging this pull request may close these issues.

exporter: refactor Clauses
2 participants